(declare-fun v () (Array (_ BitVec 32) (Array (_ BitVec 32) (_ BitVec 32))))
(declare-fun v_ () (Array (_ BitVec 32) (Array (_ BitVec 32) (_ BitVec 32))))
(assert (= v_ (store v (_ bv0 32) (select v (_ bv0 32)))))
(set-info :status sat)
(check-sat)
